COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 Jussi's Lisp axioms - as in 1982 Nov. EKL Manual
C00010 ENDMK
C⊗;
;;; Jussi's Lisp axioms - as in 1982 Nov. EKL Manual
(proof lispax) 

;;;declarations: note that t and nil are not declared - ekl knows about them
;;;since they are attached, we don't need to say things like null nil etc.

(decl car (unaryname: car) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl cdr (unaryname: cdr) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl atom (unaryname: atom) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl null (unaryname: null) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl listp (unaryname: listp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl alistp (unaryname: alistp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl sexp (unaryname: sexp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl (u v w) (type: |ground|) (sort: |listp|))

(decl (x y z) (type: |ground|) (sort: |sexp|))

(decl (xa ya za) (type: |ground|) (sort: |atom|))

(decl (a b c) (type: |ground|))

(decl (phi) (type: |ground→truthval|))

(decl cons (type: |(ground⊗ground)→ground|) (syntype: constant) (infixname: |.|)
 (prefixname: cons) (bindingpower: 850))

;;;basic axioms and sort info

(axiom |∀xa.sexp(xa)|)
(label sortinfo)

(axiom |∀u.sexp u|)
(label sortinfo)

(axiom |∀x u.listp x.u|)
(label sortinfo)

(axiom |∀u.u=nil ≡ null u|)
(label simpinfo)

(axiom |∀x y.sexp x.y|)
(label sortinfo)

(axiom |∀x y.¬atom x.y|)
(label sortinfo)

(axiom |∀x u.¬null x.u|)
(label sortinfo)

(axiom |∀x y.car (x.y) = x|)
(label simpinfo)

(axiom |∀x y.cdr (x.y) = y|)
(label simpinfo)

;;;induction

(axiom |∀phi.phi(nil)∧(∀x u.phi(u)⊃phi(x.u))⊃(∀u.phi(u))|)
(label listinduction)

(decl pars (type: |ground*|))
(axiom
 |∀nilcase def.
   ∃fun. ∀pars u.fun(u,pars)=
	         (if null u then nilcase(pars)
    			    else def(u,fun((cdr u),pars),pars))|)
(label listinductiondef)

(axiom |∀phi.(∀x.atom x ⊃ phi(x))∧(∀x y.phi(x)∧phi(y)⊃phi(x.y))⊃(∀x.phi(x))|)
(label sexpinduction)

(axiom
 |∀atomcase defsexp.
   ∃fun. ∀pars x.fun(x,pars)=
	         (if (atom x) then atomcase(x,pars)
 			      else defsexp(x,fun((car x),pars),fun((cdr x),pars),pars))|)
(label sexpinductiondef)

;;; lists of variable numbers of arguments don't require special treatment,
;;; since we have list types now

(decl list (type: |ground* → ground|) (syntype: constant))
(decl lst (type: |ground*|))
(axiom |∀x.listp(list(x))|)
(label sortinfo)

(axiom |∀x.list(x) = x.nil|)
(label simpinfo)

(axiom |∀lst.listp(list(lst))|)
(label sortinfo)

(axiom |∀x lst.list(x,lst) = x.list(lst)|)
(label simpinfo)

;;; this is lisp's append.  while it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.
 
(decl append (type: |ground⊗ground*→ground|) (syntype: constant)
      (associativity: both) (infixname: *) (bindingpower: 840))

(axiom |∀u v.listp(u*v)|)
(label sortinfo) (label listappend)

(axiom |∀u v.(u*v)=(if  (null(u)) then v else (car u) . ((cdr u)*v))|)
(label append_def)
(label definfo)

(axiom |∀u.nil*u=u|)
(label appendfacts) (label simpinfo)

(axiom |∀x u v.(x.u)*v = (x.(u*v))|)
(label appendfacts) (label simpinfo)

;;;map functions on lists

(axiom |allp = λphi u.if null u then true
       		      else if ¬phi(car u) then false
			   else allp(phi, cdr u)|)

(axiom |somep = λphi u.if null u then false
		       else if phi(car u) then true
			    else somep(phi, cdr u)|)
 
(axiom |mapcar = λfn u.if null u then nil else fn(car u).mapcar(fn, cdr u)|)

(decl (alist a0 a1 a2) (type: ground) (sort: alistp))
(axiom |∀alist. listp alist|)
(label simpinfo) (label sortinfo)
(axiom |∀alist. ¬null alist ⊃ ¬atom car alist ∧ atom car car alist|)

(axiom |∀xa y alist.alistp (xa.y).alist|)
(label mkalist)

(decl assoc (type:  |ground⊗ground → ground|) (syntype: constant))

(axiom |∀x alist. assoc(x,alist) =
                       if (null alist) then nil
                       else (if x = (car car alist) then (car alist)
                                                  else (assoc(x, cdr alist)))|)
(label definfo)

(axiom |∀x alist.sexp assoc(x,alist)|)
(label sortinfo)

(decl member (type: |ground⊗ground → truthval|) (syntype: constant))

(axiom |∀x u. member(x,u) ≡ ¬null u ∧ (x = car u ∨ member(x, cdr u))|)
(label definfo)